When developing integrated circuits that perform floating point arithmetic, designers typically base the representations of floating point (FP) numbers and the constraints on the results of arithmetic operations on published standards, such as the document IEEE Standard for Binary Floating Point Arithmetic, An American National Standard, ANSI/IEEE Std. 754-1995. Adherence to such standards guarantees that the circuitry will perform floating point arithmetic with acceptable and predictable results. Although it is a relatively straightforward task to implement floating point standards in a floating point hardware unit, designers usually make modifications in the implementation to improve performance in special cases. Because of this, it is necessary to verify compliance of the finished design with the selected standard. In many instances, errors in floating point implementation escape detection and find their way into production. Cases such as the well-known Pentium bug show that the verification process in this area is still far from being optimal. The ever-growing demand for increased performance, reduced time-to-market, and decreasing tolerance for errors all combine to make verification increasingly harder.
The term “floating point unit” herein denotes any device or system capable of performing binary floating point computations by any means including, but not limited to, hardware, firmware, programmable logic arrays, and software.
Floating point unit verification presents a unique challenge in the field of processor verification. The particular complexity of this area stems from the vast test-space, which includes many corner cases that should be targeted, and from the intricacies of the implementation of floating point operations.
One approach involves using formal methods to develop proofs of adherence to a standard. While promising, formal methods are still far from providing a complete answer to the problem. Simulation is a more traditional approach to floating point unit verification. The rationale behind verification by simulation is that one acquires confidence in the correctness of a floating point unit design by running a set of test cases that encompass a sufficiently large number of different cases, which in some sense is assumed to be a representative sample of the full space. The ability of the floating point unit design to correctly handle all cases is inferred from the correct handling of the cases actually tested. This approach is discussed, for example, in the document User Defined Coverage—A Tool Supported Methodology for Design Verification, Raanan Grinwald, Eran Harel, Michael Orgad, Shmuel Ur, and Avi Ziv, Proc. 38th Design Automation Conference (DAC38), pages 158-163, 1998. When conducting simulation, it is desirable to define a particular subspace, which is considered to be “interesting” in terms of verification, and then to generate tests selected at random out of the subspace.
Examples of algorithms that may be used for test generation may be found in the following documents:
How to Test Whether SQRT is Rounded Correctly, W. Kahan.
http://www cs.berkeley.edu/˜wkahan/SQRTest.ps;
Generation and Analysis of Hard To Round Cases for Binary Floating Point Division, Lee D. McFearin and David W. Matula, IEEE 15th Symposium on Computer Arithmetic (ARITH15), pages 119-127, 2001; and
Number-Theoretic Test Generation for Directed Rounding, Michael Parks, Proc. IEEE 14th Symp. Computer Arithmetic (AR-ITH14), pages 241-248, 1999.
Test cases developed by algorithms such as the foregoing are typically implemented on a test generator, which may optionally bias the tests based on internal testing knowledge. Such test generators are described in the following documents: Model-Based Test Generation For Processor Design Verification, Y. Lichtenstein, Y. Malka and A. Aharon, Innovative Applications of Artificial Intelligence (IAAI), AAAI Press, 1994; Constraint Satisfaction for Test Program Generation, L. Fournier, D. Lewin, M. Levinger, E. Roytman and Gil Shurek, Int. Phoenix Conference on Computers and Communications, March 1995; and Test Program Generation for Functional Verification of PowerPC Processors in IBM, A. Aharon, D. Goodman, M. Levinger, Y. Lichtenstein, Y. Malka, C. Metzger, M. Molcho and G. Shurek, 32nd Design Automation Conference, San Francisco, June 1995, pp. 279-285.
More recently, test cases have been implemented in a floating point test generator, FPgen, at the IBM Haifa Research Laboratories, as disclosed in the document A Deep Knowledge Test Generator for Floating Point Verification, S. Asaf and L. Fournier. FPgen—Technical Report H-0140, IBM Israel, 2002,
http://
domino.watson.ibm.com/library/cyberdig.nsf/Home, which is herein incorporated by reference. FPgen is an automatic floating point test generator, which receives as input the description of a floating point coverage task and outputs a random test that covers this task. A coverage task is defined by specifying a floating point instruction and a set of constraints on the inputs, the intermediate results, and the final result. For each task, the generator produces a random test that satisfies all the constraints. FPgen employs various algorithms, both analytic and heuristic, to solve the various constraint types.
Test generation for the addition instruction FP-ADD, where the input sets are described as masks, is discussed in the document Solving The Generalized Mask Constraint for Test Generation of Binary Floating Point Add Operation, Abraham Ziv and Laurent Fournier, Theoretical Computer Science, 291:183-201, 2003, which is herein incorporated by reference. While this technique is effective for mask-constrained test generation, verification of floating point units would be further advanced by an improved technique for generating meaningful range-constrained test cases.